FDL - Nuprl Lemma : linorder_functionality_wrt_iff

Nuprl Lemma : linorder_functionality_wrt_iff

T:Type, R, R':(T

T

).
(

x, y:T. R(x,y)

R'(x,y))

(Linorder(T;x,y.R(x,y))

Linorder(T;x,y.R'(x,y)))

Up rel 1, rel 1

Definitions P Q, P & Q, t T, Linorder(T;x,y.R(x;y)), x(s1,s2), P Q, P Q, , x:A. B(x), x,y. t(x;y)

Lemmas iff wf, connex functionality wrt iff, order functionality wrt iff, and functionality wrt iff, iff functionality wrt iff, connex wf, order wf